Power Programmierung/Power-Programmierung (Tewi)(1994).iso/magazine/drdobbs/1986/04/brown.pro

Text File | 1986-04-30 | 9KB | 257 lines

; File: BOYER.LIB

(PUTD 'DEFUN '(NLAMBDA (NAM$ EXP$) (PUTD NAM$ EXP$) NAM$))



(DEFUN VARIABLEP (LAMBDA (V)
  (* determine if V is a variable: if it starts with lower-case
      it is *)
  ((ATOM V)
    (GREATERP (ASCII (CAR (UNPACK V))) (ASCII `)) )
  NIL ))

(DEFUN LPAR (LAMBDA (R)
  (* return left parent *)
  (CAR R) ))

(DEFUN LLIT# (LAMBDA (R)
  (* return left litteral number *)
  (CADR R) ))

(DEFUN RPAR (LAMBDA (R)
  (* return right parent *)
  (CADDR R) ))

(DEFUN RLIT# (LAMBDA (R)
  (* return right litteral number *)
  (CAR (CDDDR R)) ))

(DEFUN NLITS (LAMBDA (R)
  (* return number of litterals *)
  (CADR (CDDDR R)) ))

(DEFUN MAXNDX (LAMBDA (R)
  (* return maximum index *)
  (CADDR (CDDDR R)) ))

(DEFUN BINDINGS (LAMBDA (R)
  (* return the bindings *)
  (CAR (CDDDR (CDDDR R))) ))

(DEFUN SETLPAR (LAMBDA (R V)
  (* set left parent *)
  (RPLACA R V) ))

(DEFUN SETLLIT# (LAMBDA (R V)
  (* set left litteral number *)
  (RPLACA (CDR R) V) ))

(DEFUN SETRPAR (LAMBDA (R V)
  (* set right parent *)
  (RPLACA (CDDR R) V) ))

(DEFUN SETRLIT# (LAMBDA (R V)
  (* set right litteral number *)
  (RPLACA (CDDDR R) V) ))

(DEFUN SETNUMLITS (LAMBDA (R V)
  (* set number of litterals *)
  (RPLACA (CDR (CDDDR R)) V) ))

(DEFUN SETMAXNDX (LAMBDA (R V)
  (* set maximum index *)
  (RPLACA (CDDR (CDDDR R)) V) ))

(DEFUN SETBINDINGS (LAMBDA (R V)
  (* set bindings *)
  (RPLACA (CDDDR (CDDDR R)) V) ))

(DEFUN INRECP (LAMBDA (R)
  (* is R an input record? *)
  (NULL (RPAR R)) ))

(DEFUN LEQP (LAMBDA (X Y)
  (* is X less than or equal to Y ? *)
  (NOT (GREATERP X Y)) ))

(DEFUN NMEMS (LAMBDA (L)
  (* return the number of members in the list L *)
  ((NULL L) 0)
  (ADD1 (NMEMS (CDR L))) ))

(DEFUN EXTRACT (LAMBDA (K L TMP)
  (* return the Kth member of L *)
  (* TMP is a local variable *)
  (LOOP
    ((ZEROP K) TMP)
    (SETQ K (SUB1 K))
    (SETQ TMP (POP L)) ) ))

(DEFUN RESOLVE (LAMBDA (CL1 I CL2 J LLIT RLIT LNDX RNDX BNDEV
    LSIGN RSIGN)
  (* resolve clause CL1 litteral I with clause CL2 litteral J
      returning a new clause record representing the resolvent:
      UNIFY will extend the binding environment: returns NIL if
      impossible *)
  (GETLIT CL1 I)
  (SETQ LLIT LITG)
  (SETQ LNDX INDEXG)
  (SETQ LSIGN SIGNG)
  (GETLIT CL2 J)
  (SETQ RLIT LITG)
  (SETQ RNDX (PLUS INDEXG (MAXNDX CL1)))
  (SETQ RSIGN SIGNG)
  (* create the new clause record *)
  (SETQ BNDEV (LIST CL1 I CL2 J (DIFFERENCE (PLUS (NLITS CL1)
      (NLITS CL2)) 2) (PLUS (MAXNDX CL1) (MAXNDX CL2)) NIL))
  (* test for opposite signs *)
  ((EQ LSIGN RSIGN) NIL)
  (* extend the environment by the unification algorithm *)
  ((UNIFY LLIT LNDX RLIT RNDX) BNDEV)
  NIL ))

(DEFUN GETLIT (LAMBDA (CL K)
  (* get the Kth litteral in clause CL: return the litteral
      gotten in LITG: and the associated index in INDEXG *)
  (* if CL is an input clause then extract the Kth litteral and
      set the index to 1 *)
  ((INRECP CL)
    (SETQ LITG (EXTRACT K (LPAR CL)))
    (SETQ SIGNG (EQ K 1))
    (SETQ INDEXG 1) )
  (* if it is in the left parent of the clause then get the
      litteral from the left parent *)
  (* this is true if K is less than the litteral last resolved
      upon in the left parent of the current clause *)
  ((LESSP K (LLIT# CL))
    (GETLIT (LPAR CL) K) )
  (* this is also true if K is less than the number of litterals
      in the left parent but in this case we must adjust K by 1
      *)
  ((LESSP K (NUMLITS (LPAR CL)))
    (GETLIT (LPAR CL) (ADD1 K)) )
  (* if the selected litteral is in the right parent but left of
      the litteral last resolved upon then get the litteral from
      the right parent with the appropriate adjustment to K *)
  ((LESSP K (PLUS (SUB1 (NUMLITS (LPAR CL))) (RLIT# CL)))
    (GETLIT (RPAR CL) (ADD1 (DIFFERENCE K (NUMLITS (LPAR CL)))))
    (* in this case adjust the index got *)
    (SETQ INDEXG (PLUS INDEXG (MAXNDX (LPAR CL)))) )
  (* otherwise the selected litteral is in the right parent to
      the right of last litteral resolved upon so adjust K
      accordingly and get the litteral *)
  (GETLIT (RPAR CL) (PLUS (DIFFERENCE K (NUMLITS (LPAR CL))) 2))
  (* and adjust the index gotten *)
  (SETQ INDEXG (PLUS INDEXG (MAXNDX (LPAR CL)))) ))

(DEFUN UNIFY (LAMBDA (TERM1 INDEX1 TERM2 INDEX2)
  (* attempt to unify TERM1 under INDEX1 with TERM2 under INDEX2
      and extend the binding environment represented in the
      global variable BNDEV: return T if successful or NIL if the
      unification is impossible *)
  (* if both terms and indices are equal then return T: no
      extension to BNDEV is needed *)
  ((EQUAL TERM1 TERM2)
    (EQ INDEX1 INDEX2)
    T )
  (* if TERM1 is a variable *)
  ((VARIABLEP TERM1)
    (* then if it is bound in the current environment *)
    ((ISBOUND TERM1 INDEX1 BNDEV)
      (* then substitute that binding and attempt to unify again
          *)
      (UNIFY TERMB INDEXB TERM2 INDEX2) )
    (* else if the variable of TERM1 occurs in TERM2 then we
        have a recursive """black" "hole""" situation so return
        NIL *)
    ((OCCUR TERM1 INDEX1 TERM2 INDEX2) NIL)
    (* else force a unification by adding the necessary binding
        and return T for success *)
    (BIND TERM1 INDEX1 TERM2 INDEX2 BNDEV)
    T )
  (* if TERM2 is a variable then swap the 2 terms and UNIFY the
      other way *)
  ((VARIABLEP TERM2)
    (UNIFY TERM2 INDEX2 TERM1 INDEX1) )
  (* otherwise if the heads of the terms unify then return the
      result of unifying the tails of the terms: the environment
      is extended as needed *)
  ((UNIFY (CAR TERM1) INDEX1 (CAR TERM2) INDEX2)
    (UNIFY (CDR TERM1) INDEX1 (CDR TERM2) INDEX2) ) ))

(DEFUN ISBOUND (LAMBDA (VAR INDEX BNDEV)
  (* determine if the variable VAR under the index INDEX is
      bound in the binding environment BNDEV: if it is then
      return T and set the free variables TERMB and INDEXB to
      the term and index respectively to which it is bound: *)
  (* otherwise return NIL and do not alter the values of TERMB and
      INDEXB *)
  (* if BNDEV is an input record then it cannot be bound so
      return NIL *)
  ((INRECP BNDEV) NIL)
  (* if VAR under INDEX is equal to the head of the binding
      environment at this level then return T and set TERMB and
      INDEXB accordingly *)
  ((EQUAL (CONS VAR INDEX) (CAR (BINDINGS BNDEV)))
    (SETQ TERMB (CADAR (BINDINGS BNDEV)))
    (SETQ INDEXB (CAR (CDDAR (BINDINGS BNDEV))))
    T )
  (* else see if it is bound in the tail of the binding
      environment at this level *)
  ((ISBOUND VAR INDEX (CDR (BINDINGS BNDEV))) T)
  (* if not then check INDEX to see whether to search the left
      or right parent binding environment *)
  ((LEQP INDEX (MAXNDX (LPAR BNDEV)))
    (* search left parent *)
    (ISBOUND VAR INDEX (LPAR BNDEV)) )
  (* search right parent *)
  ((ISBOUND VAR (DIFFERENCE INDEX (MAXNDX (LPAR BNDEV))) (RPAR
      BNDEV))
    (* adjust INDEXB accordingly *)
    (SETQ INDEXB (PLUS INDEXB (MAXNDX (LPAR BNDEV))))
    (* and return success *)
    T )
  (* all possible approaches failed so return NIL for not bound *)
  NIL ))

(DEFUN OCCUR (LAMBDA (V I TERM J)
  (* see if the variable V under the index I occurs in the term
      TERM under the index J and return T or NIL *)
  (* if TERM is a variable *)
  ((VARIABLEP TERM)
    (* then if it is bound *)
    ((ISBOUND TERM J BNDEV)
      (* then make the substitution and test for occurance *)
      (OCCUR V I TERMB INDEXB) )
    (* if V equals TERM *)
    ((EQ V TERM)
      (* then return T if I=J else NIL *)
      (EQ I J) ) )
  (* if TERM is atomic and not a variable *)
  (* then it is a constant so return NIL *)
  ((ATOM TERM) NIL)
  (* otherwise if V under I occurs in the head of TERM under J
      then return T *)
  ((OCCUR V I (CAR TERM) J) T)
  (* otherwise return T if V under I occurs in the tail of TERM
      under J and NIL otherwise *)
  (OCCUR V I (CDR TERM) J) ))

(DEFUN BIND (LAMBDA (V I TERM J BNDEV)
  (* bind V under I to TERM under J in BNDEV *)
  (SETBINDINGS BNDEV (CONS (CONS (CONS V I) (CONS TERM J))
      (BINDINGS BNDEV))) ))

(DEFUN * (LAMBDA COMMENTS
  NIL ))

(DEFUN MAKECL (LAMBDA (CL)
  (* make a clause record out of the expression CL *)
  (LIST CL 0 NIL 0 (NMEMS CL) 1 NIL) ))


(RDS)
AKECL (LAMBDA (CL)
  (* make a clause record out of the expression CL *)
  (LI